Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add kani harness and auto-generated bolero harnesses #227

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Add kani harness and auto-generated bolero harnesses #227

wants to merge 2 commits into from

Conversation

cvick32
Copy link

@cvick32 cvick32 commented Sep 5, 2024 •
edited
Loading

Summary of the PR

Adds failing 5 Kani harnesses and 7 auto-generated Bolero harnesses.

Running cargo kani fails with:

SUMMARY:
 ** 1 of 334 failed (7 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/ec2-user/.rustup/toolchains/nightly-2024-05-28-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs", line 1679, in std::result::unwrap_failed

VERIFICATION:- FAILED
Verification Time: 28.542933s

Summary:
Verification failed for - fam::kani_harnesses::prove_capacity
Verification failed for - fam::kani_harnesses::prove_len
Verification failed for - fam::kani_harnesses::prove_as_fam_struct_ptr
Verification failed for - fam::kani_harnesses::prove_into_raw
Verification failed for - fam::kani_harnesses::prove_as_mut_fam_struct
Complete - 0 successfully verified harnesses, 5 failures, 5 total.

Requirements

Before submitting your PR, please make sure you addressed the following
requirements:

  • All commits in this PR have Signed-Off-By trailers (with
    git commit -s), and the commit message has max 60 characters for the
    summary and max 75 characters for each description line.
  • All added/changed functionality has a corresponding unit/integration
    test.
  • All added/changed public-facing functionality has entries in the "Upcoming
    Release" section of CHANGELOG.md (if no such section exists, please create one).
  • Any newly added unsafe code is properly documented.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@liujing2 liujing2 Awaiting requested review from liujing2 liujing2 will be requested when the pull request is marked ready for review liujing2 is a code owner

@sameo sameo Awaiting requested review from sameo sameo will be requested when the pull request is marked ready for review sameo is a code owner

@andreeaflorescu andreeaflorescu Awaiting requested review from andreeaflorescu andreeaflorescu will be requested when the pull request is marked ready for review andreeaflorescu is a code owner

@jiangliu jiangliu Awaiting requested review from jiangliu jiangliu will be requested when the pull request is marked ready for review jiangliu is a code owner

@roypat roypat Awaiting requested review from roypat roypat will be requested when the pull request is marked ready for review roypat is a code owner

@ShadowCurse ShadowCurse Awaiting requested review from ShadowCurse ShadowCurse will be requested when the pull request is marked ready for review ShadowCurse is a code owner

At least 2 approving reviews are required to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@cvick32